\begin{tabbing}
$\forall$${\it ds}$:fpf(Id; $x$.Type), ${\it da}$:fpf(Knd; $k$.Type), ${\it es}$:event\_system\{i:l\}, $i$:Id, $e_{1}$,$e_{2}$:\{\=$e$:es{-}E(${\it es}$)$\mid$ \+
\\[0ex]loc($e$) = $i$\} .
\-\\[0ex]($\forall$$x$:Id. subtype\_rel(es{-}vartype(${\it es}$; $i$; $x$); fpf{-}cap(${\it ds}$; id{-}deq; $x$; top)))
\\[0ex]$\Rightarrow$ \=($\forall$$e$:es{-}E(${\it es}$). \+
\\[0ex](loc($e$) = $i$)
\\[0ex]$\Rightarrow$ subtype\_rel(es{-}valtype(${\it es}$; $e$); fpf{-}cap(${\it da}$; Kind{-}deq; es{-}kind(${\it es}$; $e$); top)))
\-\\[0ex]$\Rightarrow$ \=($\forall$${\it ks}$:(Knd List), $T$:Type, $z$:$T$, $g$:(\=$k$:\{$k$:Knd$\mid$ ($k$ $\in$ ${\it ks}$)\} $\rightarrow$decl{-}state(${\it ds}$)$\rightarrow$\+\+
\\[0ex]fpf{-}cap(${\it da}$; Kind{-}deq; $k$; top)$\rightarrow$$T$$\rightarrow$$T$).
\-\\[0ex]es{-}trans{-}state{-}from\{i:l\}(${\it es}$;${\it ks}$;$g$;$z$;$e_{1}$;$e_{2}$) $\in$ $T$)
\-
\end{tabbing}